(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v19 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i11 Int)
(declare-const v21 Bool)
(declare-const i14 Int)
(assert (or (= (= v21 v15 v5 v19 v16 v3) v10 (xor (and v7 v16 v9 v2 v13 v2 v11 v19 v2 v6 v13) v3 v12 v0 (= v21 v15 v5 v19 v16 v3) v13 v4 v5 v9) v9 (= 3 i14) v7 v16 v7 (xor (and v7 v16 v9 v2 v13 v2 v11 v19 v2 v6 v13) v3 v12 v0 (= v21 v15 v5 v19 v16 v3) v13 v4 v5 v9) (< 85 i1) v12) v7 (distinct v1 v13 v19 v10 v6)))
(assert (or (> (- i11 i2 i14 i11 i5) 895) v1 v14))
(assert (or v21 v19 v19))
(check-sat)
